;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "irotate.lisp")
(require "iimage.lisp")

(module MRotate
  (import IImage)
  
  
  (defun GetRotatedPosition(x y width height mode)
    (cond 
      ((string-equal mode "RIGHT") (list (+ (- height y) 1) x)) 
      ((string-equal mode "LEFT")  (list y (+ (- width x) 1)))
      ((string-equal mode "FLIP")  (list (+ (- width x) 1) (+ (- height y) 1)))))
  
  (defun RotatePixel (originalTree newTree x y width height mode)
    (let* ((nextX  (getNextXCoordinate x width))
           (nextY  (getNextYCoordinate x y width))
           (pixel  (getPixel originalTree x y))
           (pixelR (car   pixel))
           (pixelG (cadr  pixel))
           (pixelB (caddr pixel))
           (newLoc (GetRotatedPosition x y width height mode))
           (newX   (car  newLoc))
           (newY   (cadr newLoc)))
        (if (isValidPixel nextX nextY width height)
            (RotatePixel originalTree (insertPixel newTree newX newY pixelR pixelG pixelB) nextX nextY width height mode)
            (insertPixel newTree newX newY pixelR pixelG pixelB))))
  
  (defun MainRotate(tree args)
    (let* ((angle  (car args))
           (mode   (mod (floor angle 90) 4))
           (width  (getWidth tree))
           (height (getHeight tree)))
      (if (equal (mod angle 90) 0)
          (cond 
            ((equal mode 0) (mv tree (list "Successfully rotated 0 degrees.")));Do Nothing (roate 0 degrees)
            ((equal mode 1) (mv (RotatePixel tree (setHeight (setWidth tree height) width) 1 height width height "RIGHT") (list "Successfully rotated 90 degrees clockwise."))) ;Rotate 90 degrees right
            ((equal mode 2) (mv (RotatePixel tree tree 1 height width height "FLIP")  (list "Successfully rotated 180 degrees."))) ;Rotate 180 degrees
            ((equal mode 3) (mv (RotatePixel tree (setHeight (setWidth tree height) width) 1 height width height "LEFT")  (list "Successfully rotated 90 degrees counter-clockwise."))));Rotate 90 degrees left
          (mv tree (list "Invalid rotation angle. Must be a multiple of 90.")))))
  
          
  
  (export IRotate))